<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
            "http://www.w3.org/TR/REC-html40/loose.dtd">
<HTML>
<HEAD>



<META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
<META name="GENERATOR" content="hevea 1.08">
<LINK rel="stylesheet" type="text/css" href="tutorial.css">
<TITLE>
Propia
</TITLE>
</HEAD>
<BODY >
<A HREF="tutorial109.html"><IMG SRC ="previous_motif.gif" ALT="Previous"></A>
<A HREF="tutorial107.html"><IMG SRC ="contents_motif.gif" ALT="Up"></A>
<A HREF="tutorial111.html"><IMG SRC ="next_motif.gif" ALT="Next"></A>
<HR>

<H2 CLASS="section"><A NAME="htoc214">15.3</A>&nbsp;&nbsp;Propia</H2><UL>
<LI><A HREF="tutorial110.html#toc106">How to Use Propia</A>
<LI><A HREF="tutorial110.html#toc107">Propia Implementation</A>
<LI><A HREF="tutorial110.html#toc108">Propia and Related Techniques</A>
</UL>

<A NAME="secpropia"></A>
<A NAME="@default386"></A>
<A NAME="@default387"></A>
Propia is an implementation of <EM>Generalised Propagation</EM>
which is described in the paper [<A HREF="tutorial133.html#LeProvost93b"><CITE>14</CITE></A>].<BR>
<BR>
<A NAME="toc106"></A>
<H3 CLASS="subsection"><A NAME="htoc215">15.3.1</A>&nbsp;&nbsp;How to Use Propia</H3>
<A NAME="@default388"></A>
In principle Propia propagates information from an annotated goal by
finding all solutions to the goal and extracting any information that
is common to all the different solutions.
(In practice, as we shall see later, Propia does not typically need to
find all the solutions.)<BR>
<BR>
The &#8220;common&#8221; information that can be extracted depends upon what
constraint solvers are used when evaluating the underlying
un-annotated ECL<SUP><I>i</I></SUP>PS<SUP><I>e</I></SUP> goal. To illustrate this, consider another
simple example.
<BLOCKQUOTE CLASS="quote">
<PRE CLASS="verbatim">
p(1,3).
p(1,4).

?-  p(X,Y) infers most.
</PRE></BLOCKQUOTE>
If the <TT>ic</TT> library is not loaded when this query is
invoked, then the information propagated by Propia is that <I>X</I>=1.
If, on the other hand, <TT>ic</TT> is loaded, then more common
information is propagated. Not only does Propia propagate <I>X</I>=1 but
also the domain of <I>Y</I> is tightened from <CODE>-inf..inf</CODE> to 
<CODE>3..4</CODE>. (In this case the additional common information is that
<I>Y</I> &#8800; 0, <I>Y</I> &#8800; 1, <I>Y</I> &#8800; 2 and so on for all values except 3
and 4!)<BR>
<BR>
<A NAME="@default389"></A>
<A NAME="@default390"></A>
<A NAME="@default391"></A>
<A NAME="@default392"></A>
Any goal <CODE>Goal</CODE> in an ECL<SUP><I>i</I></SUP>PS<SUP><I>e</I></SUP> program, can be transformed into a
constraint by annotating it thus: <CODE>Goal infers Parameter</CODE>.
Different behaviours can be specified with different parameters, viz:
<UL CLASS="itemize"><LI CLASS="li-itemize">
<CODE>Goal infers most</CODE><BR>
Propagates all common information produced by the loaded solvers
<LI CLASS="li-itemize"><CODE>Goal infers unique</CODE><BR>
Fails if there is no solution, propagates the solution if it is
unique, and succeeds without propagating further information if there
is more than one solution.
<LI CLASS="li-itemize"><CODE>Goal infers consistent</CODE><BR>
Fails if there is no solution, and propagates no information otherwise 
</UL>
<A NAME="@default393"></A>
These behaviours are nicely illustrated by the crossword demonstration
program <CODE>crossword</CODE> in the examples code directory.
There are 72 ways to complete the crossword grid with words from the
accompanying directory. 
For finding all 72 solutions,
the comparative performance of the different annotations is given in the
table <EM>Comparing Annotations</EM>.
<BLOCKQUOTE CLASS="table"><DIV CLASS="center"><HR WIDTH="80%" SIZE=2></DIV>
<DIV CLASS="center">
<TABLE BORDER=1 CELLSPACING=0 CELLPADDING=1>
<TR><TD ALIGN=center NOWRAP>Annotation</TD>
<TD ALIGN=center NOWRAP>CPU time (secs)</TD>
</TR>
<TR><TD ALIGN=center NOWRAP>consistent</TD>
<TD ALIGN=center NOWRAP>13.3</TD>
</TR>
<TR><TD ALIGN=center NOWRAP>unique</TD>
<TD ALIGN=center NOWRAP>2.5</TD>
</TR>
<TR><TD ALIGN=center NOWRAP>most</TD>
<TD ALIGN=center NOWRAP>9.8</TD>
</TR>
<TR><TD ALIGN=center NOWRAP>ac</TD>
<TD ALIGN=center NOWRAP>0.3</TD>
</TR></TABLE>
</DIV>
<BR>
<BR>
<DIV CLASS="center">Table 15.1: Comparing Annotations</DIV><BR>
<BR>

<DIV CLASS="center"><HR WIDTH="80%" SIZE=2></DIV></BLOCKQUOTE>
The example program also illustrates the effect of specifying the waking
conditions for Propia. By only waking a Propia constraint when it
becomes instantiated, the time to solve the crossword problem can be
changed considerably. For example by changing the annotation from
<CODE>Goal infers most</CODE> to 
<CODE>suspend(Goal,4,Goal-&gt;inst) infers most</CODE> 
the time needed to find all solutions goes down from 10 seconds to
just one second.<BR>
<BR>
For other problems, such as the square tiling problem in the example
directory, the fastest version is the 
one using <CODE>infers consistent</CODE>. To find the best Propia
annotation it is necessary to experiment with the current problem
using realistic data sets.<BR>
<BR>

	<BLOCKQUOTE CLASS="figure"><DIV CLASS="center"><HR WIDTH="80%" SIZE=2></DIV>
	<DIV CLASS="center">
	<TABLE CELLPADDING=10>
<TR><TD BGCOLOR="#DB9370">
	
Propia extracts information from a procedure which may be defined by
multiple ECL<SUP><I>i</I></SUP>PS<SUP><I>e</I></SUP> clauses. 
The information to be extracted is
controlled by the Propia annotation.

	</TD>
</TR></TABLE>
	</DIV>
	<BR>
<BR>
<DIV CLASS="center">Figure 15.3: Transforming Procedures to Constraints</DIV><BR>
<BR>

	<DIV CLASS="center"><HR WIDTH="80%" SIZE=2></DIV></BLOCKQUOTE>
<A NAME="toc107"></A>
<H3 CLASS="subsection"><A NAME="htoc216">15.3.2</A>&nbsp;&nbsp;Propia Implementation</H3>
In this section we describe how Propia works.<BR>
<BR>

<H4 CLASS="subsubsection">Outline</H4>
When a goal is annotated as a Propia constraint, eg. 
<CODE>p(X,Y) infers most</CODE>, first the goal <CODE>p(X,Y)</CODE> is in effect 
evaluated in the normal way by ECL<SUP><I>i</I></SUP>PS<SUP><I>e</I></SUP>.
However Propia does not stop at the first solution, but continues to
find more and more solutions, each time combining the information from
the solutions retrieved.
When all the information has been accumulated, Propia propagates this
information (either by narrowing the domains of variables in the goal,
or partially instantiating them).<BR>
<BR>
Propia then suspends the goal again, until the variables become
further constrained, at which point it wakes, extracts information
from solutions to the more constrained goal, propagates it, and
suspends again.<BR>
<BR>
If Propia detects that the goal is entailed (i.e. the goal would
succeed whichever way the variables were instantiated), then after
propagation it does not suspend any more.<BR>
<BR>

<H4 CLASS="subsubsection">Most Specific Generalisation</H4>
<A NAME="@default394"></A>
<A NAME="@default395"></A>
Propia works by treating its input both as a <EM>goal</EM> to be called,
and as a term which can be manipulated as data.
As with any ECL<SUP><I>i</I></SUP>PS<SUP><I>e</I></SUP> goal, when executed its result is a further
instantiation of the term. 
For example the first result of calling <CODE>member(X,[a,b,c])</CODE> is
to further instantiate the term yielding <CODE>member(a,[a,b,c])</CODE>.
This instantiated term represents the (first) solution to the goal.<BR>
<BR>
Propia combines information from the solutions to a goal using their
<EM>most specific generalisation</EM> (<EM>MSG</EM>).
The MSG of two terms is a term
that can be instantiated (in different ways) to either of the two
terms. For example
<I>p</I>(<I>a</I>,<I>f</I>(<I>Y</I>)) is the MSG of <I>p</I>(<I>a</I>,<I>f</I>(<I>b</I>)) and <I>p</I>(<I>a</I>,<I>f</I>(<I>c</I>)).
This is the meaning of <EM>generalisation</EM>. 
The meaning of <EM>most specific</EM> is that any other term that
generalises the two terms, is more general than the MSG.
For example, any other term that generalises <I>p</I>(<I>a</I>,<I>f</I>(<I>b</I>) and
<I>p</I>(<I>a</I>,<I>f</I>(<I>c</I>)) can be instantiated to <I>p</I>(<I>a</I>,<I>f</I>(<I>Y</I>)).
The MSG of two terms captures only information that is common to both
terms (because it generalises the two terms), and it captures all the
information possible in the two terms (because it is the most specific
generalisation).<BR>
<BR>
Some surprising information is caught by the MSG. For example the MSG
of <I>p</I>(0,0) and <I>p</I>(1,1) is <I>p</I>(<I>X</I>,<I>X</I>).
We can illustrate this being exploited by Propia in the following
example:

	<TABLE CELLPADDING=10>
<TR><TD BGCOLOR="#CCCCFF">
	<BLOCKQUOTE CLASS="quote"><PRE>
% Definition of logical conjunction
conj(1,1,1).
conj(1,0,0).
conj(0,1,0).
conj(0,0,0).

conjtest(X,Z) :-
    conj(X,Y,Z) infers most,
    X=Y.
</PRE></BLOCKQUOTE></TD>
</TR></TABLE>
The test succeeds, recognising that <I>X</I> must take the same truth value
as <I>Z</I>. Running this in ECL<SUP><I>i</I></SUP>PS<SUP><I>e</I></SUP> yields:
<BLOCKQUOTE CLASS="quote">
<PRE CLASS="verbatim">
[eclipse]: conjtest(X,Z).
X = X
Z = X
Delayed goals:
        conj(X, X, X) infers most
Yes (0.00s cpu)
</PRE></BLOCKQUOTE>
If the <TT>ic</TT> library is loaded more information can be extracted,
because the MSG of 0 and 1 is a variable with domain <CODE>0..1</CODE>.
Thus the result of the above example is not only to equate <I>X</I> and <I>Z</I>
but to associate with them the domain <CODE>0..1</CODE>.<BR>
<BR>
The MSG of two terms depends upon what information is expressible in
the MSG term. As the above example shows, if the term can employ
variable domains the MSG is more precise. <BR>
<BR>
By choosing the class of terms in which the MSG can be
expressed, we can capture more or less information in the MSG.
If, for example, we allow only terms of maximum depth 1 in the class,
then MSG can only capture functor and arity.
In this case the MSG of <I>f</I>(<I>a</I>,1) and <I>f</I>(<I>a</I>,2) is simply <I>f</I>(<SUB>,</SUB><SUB>)</SUB>, even
though there is more shared information at the next depth.<BR>
<BR>
In fact the class of terms can be extended to a lattice, by
introducing a bottom &perp; and a top &#8868;. 
&perp; is a term carrying no
information; &#8868; is a term representing inconsistent information;
the 
meet of two terms is the result of unifying them; and their join is
their MSG.<BR>
<BR>

<H4 CLASS="subsubsection">The Propia Algorithm</H4>
We can now specify the Propia algorithm more precisely.
The Propia constraint is 
<PRE CLASS="verbatim">Goal infers Parameter </PRE>
<UL CLASS="itemize"><LI CLASS="li-itemize">
Set <I>OutTerm</I> := &#8868;
<LI CLASS="li-itemize">Repeat
<UL CLASS="itemize"><LI CLASS="li-itemize">
Find a solution <I>S</I> to <I>Goal</I> which is <EM>not</EM> an instance of
<I>OutTerm</I> 
<LI CLASS="li-itemize">Find the MSG, in the class specified by <CODE>Parameter</CODE>, 
of <I>OutTerm</I> and <I>S</I>. Call it <I>MSG</I>
<LI CLASS="li-itemize">Set <I>OutTerm</I> := <I>MSG</I>
</UL>
until either <I>Goal</I> is an instance of <I>OutTerm</I>, or no such
solution remains 
<LI CLASS="li-itemize">Return <I>OutTerm</I>
</UL>
When <CODE>infers most</CODE> is being handled, the class of terms admitted
for the MSG is the biggest class expressible in terms of the currently
loaded solvers. In case <I>ic</I> is loaded, this includes variable
domain, but otherwise it includes any ECL<SUP><I>i</I></SUP>PS<SUP><I>e</I></SUP> term without variable
attributes.<BR>
<BR>
The algorithm supports <CODE>infers consistent</CODE> by admitting only the
two terms &#8868; and &perp; in the MSG class.
<CODE>infers unique</CODE> is a variation of the algorithm in which the
first step <I>OutTerm</I> := &#8868; is changed to finding a first solution
<I>S</I> to <I>Goal</I> and initialising <I>OutTerm</I> := <I>S</I>.<BR>
<BR>
Propia's termination is dramatically improved by the check that the
next solution found is not an 
instance of <I>OutTerm</I>. In the absence of domains, there is no
infinite sequence of terms that strictly generalise each other.
Moreover, if
the variables in <I>Goal</I> have finite domains, the same result holds. 
Thus, because of this check, Propia will terminate as long as each
call of <I>Goal</I> terminates. <BR>
<BR>
For example the Propia constraint 
<CODE>member(Var,List) infers Parameter</CODE> will 
always terminate, if each call of <CODE>member(Var,List)</CODE> does, even in
case 
<CODE>member(Var,List)</CODE> has infinitely many solutions!<BR>
<BR>

	<BLOCKQUOTE CLASS="figure"><DIV CLASS="center"><HR WIDTH="80%" SIZE=2></DIV>
	<DIV CLASS="center">
	<TABLE CELLPADDING=10>
<TR><TD BGCOLOR="#DB9370">
	
Propia computes the Most Specific Generalisation (MSG) of the set of
solutions to a procedure. It does so without, necessarily,
backtracking through all the solutions to the procedure.
The MSG depends upon the annotation of the Propia call.

	</TD>
</TR></TABLE>
	</DIV>
	<BR>
<BR>
<DIV CLASS="center">Figure 15.4: Most Specific Generalisation</DIV><BR>
<BR>

	<DIV CLASS="center"><HR WIDTH="80%" SIZE=2></DIV></BLOCKQUOTE>
<A NAME="toc108"></A>
<H3 CLASS="subsection"><A NAME="htoc217">15.3.3</A>&nbsp;&nbsp;Propia and Related Techniques</H3>
If the finite domain solver is loaded then <CODE>Goal infers most</CODE> prunes
the variable domains so every value is supported by values in the
domains of the other variables. If every problem constraint was
annotated this way, then Propia would enforce arc consistency.<BR>
<BR>
<A NAME="@default396"></A>
Propia generalises traditional arc consistency in two ways. Firstly
it admits n-ary constraints, and secondly it handles predicates
defined by rules, as well as ground facts. In the special case that
the goal can be &#8220;unfolded&#8221; into a finite set of ground solutions,
this can be exploited by using <CODE>infers ac</CODE> to make Propia run
more efficiently. When called with parameter <CODE>infers ac</CODE>,
Propia simply finds all solutions and 
applies n-ary arc-consistency to the resulting tables.<BR>
<BR>
<A NAME="@default397"></A>
Propia also generalises <EM>constructive disjunction</EM>. Constructive
disjunction could be applied in case the
predicate was unfolded into a finite set of solutions, where each
solution was expressed using <TT>ic</TT> constraints (such as equations,
inequations etc.).
Propia can also handle recursively defined predicates, like
<CODE>member</CODE>, exampled above, which may have an infinite number of
solutions. <BR>
<BR>
<HR>
<A HREF="tutorial109.html"><IMG SRC ="previous_motif.gif" ALT="Previous"></A>
<A HREF="tutorial107.html"><IMG SRC ="contents_motif.gif" ALT="Up"></A>
<A HREF="tutorial111.html"><IMG SRC ="next_motif.gif" ALT="Next"></A>
</BODY>
</HTML>
